i:Id, T:Type, v:T, x:Id.
@i: x : T initially x = v  Dsys
& (D:Dsys.
& (@i: x : T initially x = v  D  D realizes es. vartype(i;x)  T & x initially@i  = v) 

latex

Definitions	t  T, x:AB(x), x:A. B(x), x initially@i , vartype(i;x), s = t, Type, Prop, A & B, es is an event system of D, ES, {x:A| B(x) }, x.A(x), {T}, P  Q, x. t(x), Dsys, D1  D2, D realizes es. P(es), Id, , MsgA, a = b, if b t else f fi, @i: A, @i: x:T initially x = v, x : t initially x = v
Lemmas	init-rule, ifthenelse wf, eq id wf, msga wf, ma-single-init wf, ma-empty wf, Id wf, dsys wf, realizes-monotone-wrt-sub, event system wf, d-es wf, es-vartype wf, es-initially wf